/* This file is part of Gralog, Copyright (c) 2016-2018 LaS group, TU Berlin.
 * License: https://www.gnu.org/licenses/gpl.html GPL version 3 or later. */
package gralog.npcompleteness.propositionallogic.formula;

import java.util.HashMap;
import java.util.Set;

/**
 *
 */
public class PropositionalLogicOr extends PropositionalLogicFormula {

    public PropositionalLogicFormula left;
    public PropositionalLogicFormula right;

    public PropositionalLogicOr(PropositionalLogicFormula left,
        PropositionalLogicFormula right) {
        this.left = left;
        this.right = right;
    }

    @Override
    public String toString() {
        String r = right.toString();
        if (right instanceof PropositionalLogicOr)
            r = "(" + r + ")";
        return left.toString() + " ∨ " + r;
    }

    @Override
    public boolean isAClause() {
        return left.isAClause() && right.isAClause();
    }

    @Override
    public boolean isAClause3() {
        if (!isAClause())
            return false;

        if (left instanceof PropositionalLogicOr) {
            PropositionalLogicOr lOr = (PropositionalLogicOr) left;
            return right.isLiteral() && lOr.left.isLiteral() && lOr.right.isLiteral();
        }

        if (right instanceof PropositionalLogicOr) {
            PropositionalLogicOr rOr = (PropositionalLogicOr) right;
            return left.isLiteral() && rOr.left.isLiteral() && rOr.right.isLiteral();
        }

        return left.isLiteral() && right.isLiteral(); // 2-SAT
    }

    @Override
    public void getLiterals(Set<PropositionalLogicFormula> literals) {
        left.getLiterals(literals);
        right.getLiterals(literals);
    }

    @Override
    public void getVariables(Set<String> vars) {
        left.getVariables(vars);
        right.getVariables(vars);
    }

    @Override
    protected PropositionalLogicFormula conjunctiveNormalForm(Integer varId,
        HashMap<PropositionalLogicFormula, String> varIdx) {
        String myName = "v" + varId;
        ++varId;
        varIdx.put(this, myName);
        PropositionalLogicFormula leftCnf = left.conjunctiveNormalForm(varId, varIdx);
        final String leftName = varIdx.get(left);
        PropositionalLogicFormula rightCnf = right.conjunctiveNormalForm(varId, varIdx);
        final String rightName = varIdx.get(right);

        PropositionalLogicFormula result
            = new PropositionalLogicAnd(
                new PropositionalLogicAnd(
                    new PropositionalLogicOr(
                        new PropositionalLogicOr(
                            new PropositionalLogicVariable(leftName),
                            new PropositionalLogicVariable(rightName)
                        ),
                        new PropositionalLogicNot(new PropositionalLogicVariable(myName))
                    ),
                    new PropositionalLogicOr(
                        new PropositionalLogicOr(
                            new PropositionalLogicVariable(leftName),
                            new PropositionalLogicNot(new PropositionalLogicVariable(rightName))
                        ),
                        new PropositionalLogicNot(new PropositionalLogicVariable(myName))
                    )
                ),
                new PropositionalLogicAnd(
                    new PropositionalLogicOr(
                        new PropositionalLogicOr(
                            new PropositionalLogicNot(new PropositionalLogicVariable(leftName)),
                            new PropositionalLogicVariable(rightName)
                        ),
                        new PropositionalLogicNot(new PropositionalLogicVariable(myName))
                    ),
                    new PropositionalLogicOr(
                        new PropositionalLogicOr(
                            new PropositionalLogicNot(new PropositionalLogicVariable(leftName)),
                            new PropositionalLogicNot(new PropositionalLogicVariable(rightName))
                        ),
                        new PropositionalLogicVariable(myName)
                    )
                )
            );

        if (leftCnf != null)
            result = new PropositionalLogicAnd(leftCnf, result);
        if (rightCnf != null)
            result = new PropositionalLogicAnd(rightCnf, result);
        return result;
    }
}
